$\forall$$D$:Dsys, $i$:Id, $s$:M($i$).(timed)state, $k$:Knd, $v$:d{-}decl($D$;$i$)($k$).
\\[0ex]Feasible($D$) $\Rightarrow$ (next{-}world{-}state($D$;$i$;$s$;$k$;$v$) $\in$ d{-}world{-}state($D$;$i$))